Nuprl Lemma : assert-dectt 0,22
p:Prop, d:Dec(p). dectt(d)  p 
latex

Definitionsx:A. B(x), dectt(d), Dec(P), P  Q, b, True, P  Q, P & Q, P  Q, t  T, Prop, A, P  Q, False
Lemmasfalse wf, true wf, decidable wf

origin